Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar18/HMSLASHt009.trs

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

Q is empty.

↳ QTRS

  ↳ Non-Overlap Check

Q restricted rewrite system:
The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

Q is empty.

The TRS is non-overlapping. Hence, we can switch to innermost.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

Using Dependency Pairs [1,13] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b3, i3)
START₁(i) -> BUSY₇(F, closed, stop, false, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b2, i2)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b1, i1)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b3, i3)
START₁(i) -> BUSY₇(F, closed, stop, false, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b2, i2)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> OR₂(b1, i1)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 4 less nodes.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

IDLE₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> BUSY₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)

The remaining pairs can at least by weakly be oriented.

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x7
S = S
closed = closed
stop = stop
true = true
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x7
down = down
newbuttons₄(x1, x2, x3, x4) = newbuttons₁(x4)
or₂(x1, x2) = or₂(x1, x2)
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

down > S > newbuttons₁ > or₂ > true > closed > B > open
down > S > newbuttons₁ > or₂ > true > stop > B > open
down > S > newbuttons₁ > or₂ > true > false > B > open
down > S > newbuttons₁ > or₂ > true > up > B > open
down > S > FS > closed > B > open
down > S > FS > up > B > open
down > BF > F > newbuttons₁ > or₂ > true > closed > B > open
down > BF > F > newbuttons₁ > or₂ > true > stop > B > open
down > BF > F > newbuttons₁ > or₂ > true > false > B > open
down > BF > F > newbuttons₁ > or₂ > true > up > B > open
empty > open

The following usable rules [14] were oriented:

or₂(true, b) -> true
or₂(false, b) -> b

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> IDLE₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 1 SCC with 3 less nodes.

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

BUSY₇(B, d, stop, true, b2, b3, i) -> IDLE₇(B, open, stop, false, b2, b3, i)

The remaining pairs can at least by weakly be oriented.

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x4
S = S
closed = closed
stop = stop
true = true
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x4
down = down
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

up > true > S > closed > stop > B > BF > open
up > true > S > closed > down > B > BF > open
up > true > S > closed > down > FS > open
up > true > S > false > stop > B > BF > open
up > true > S > false > down > B > BF > open
up > true > S > false > down > FS > open
up > true > F > stop > B > BF > open
up > true > F > down > B > BF > open
up > true > F > down > FS > open
empty > open

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

BUSY₇(S, d, stop, b1, b2, true, i) -> IDLE₇(S, open, stop, b1, b2, false, i)

The remaining pairs can at least by weakly be oriented.

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x6
S = S
closed = closed
stop = stop
true = true
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x6
down = down
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

closed > stop > true > B > false > S > down > open
closed > stop > F > BF > B > false > S > down > open
closed > FS > up > true > B > false > S > down > open
closed > FS > up > F > BF > B > false > S > down > open
empty > open

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

BUSY₇(F, d, stop, b1, true, b3, i) -> IDLE₇(F, open, stop, b1, false, b3, i)

The remaining pairs can at least by weakly be oriented.

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x5
S = S
closed = closed
stop = stop
true = true
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x5
down = down
B = B
open = open
F = F
up = up
BF = BF
FS = FS
empty = empty

Lexicographic Path Order [19].
Precedence:

stop > true > closed > down > S > open
stop > true > closed > down > B > BF > open
stop > true > closed > down > F > BF > open
stop > true > closed > FS > F > BF > open
stop > true > closed > FS > up > S > open
stop > true > closed > FS > up > BF > open
stop > true > false > down > S > open
stop > true > false > down > B > BF > open
stop > true > false > down > F > BF > open
stop > true > false > FS > F > BF > open
stop > true > false > FS > up > S > open
stop > true > false > FS > up > BF > open
empty > open

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be strictly oriented and are deleted.

BUSY₇(B, open, stop, false, b2, b3, i) -> IDLE₇(B, closed, stop, false, b2, b3, i)
BUSY₇(F, open, stop, b1, false, b3, i) -> IDLE₇(F, closed, stop, b1, false, b3, i)
BUSY₇(S, open, stop, b1, b2, false, i) -> IDLE₇(S, closed, stop, b1, b2, false, i)

The remaining pairs can at least by weakly be oriented.

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)

Used ordering: Combined order from the following AFS and order.
BUSY₇(x1, x2, x3, x4, x5, x6, x7) = x2
S = S
closed = closed
stop = stop
true = true
false = false
IDLE₇(x1, x2, x3, x4, x5, x6, x7) = x2
down = down
B = B
up = up
F = F
BF = BF
FS = FS
open = open
empty = empty

Lexicographic Path Order [19].
Precedence:

down > closed
up > S > closed
up > stop > closed
up > true > closed
up > false > closed
up > B > closed
up > F > closed
up > BF > closed
up > FS > closed
open > closed
empty > closed

The following usable rules [14] were oriented: none

↳ QTRS

  ↳ Non-Overlap Check

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ QDP

              ↳ QDPOrderProof

                ↳ QDP

                  ↳ DependencyGraphProof

                    ↳ QDP

                      ↳ QDPOrderProof

                        ↳ QDP

                          ↳ QDPOrderProof

                            ↳ QDP

                              ↳ QDPOrderProof

                                ↳ QDP

                                  ↳ QDPOrderProof

                                    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

BUSY₇(S, closed, stop, true, false, false, i) -> IDLE₇(S, closed, down, true, false, false, i)
BUSY₇(B, closed, stop, false, false, true, i) -> IDLE₇(B, closed, up, false, false, true, i)
BUSY₇(F, closed, down, b1, false, b3, i) -> IDLE₇(BF, closed, down, b1, false, b3, i)
BUSY₇(FS, closed, down, b1, b2, b3, i) -> IDLE₇(F, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, up, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
BUSY₇(S, closed, down, b1, b2, true, i) -> IDLE₇(S, closed, stop, b1, b2, true, i)
BUSY₇(S, closed, stop, b1, true, false, i) -> IDLE₇(S, closed, down, b1, true, false, i)
BUSY₇(F, closed, up, b1, false, b3, i) -> IDLE₇(FS, closed, up, b1, false, b3, i)
BUSY₇(B, closed, stop, false, true, b3, i) -> IDLE₇(B, closed, up, false, true, b3, i)
BUSY₇(F, closed, stop, true, false, b3, i) -> IDLE₇(F, closed, down, true, false, b3, i)
BUSY₇(F, closed, stop, false, false, true, i) -> IDLE₇(F, closed, up, false, false, true, i)
BUSY₇(BF, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, down, b1, b2, b3, i)
BUSY₇(F, closed, down, b1, true, b3, i) -> IDLE₇(F, closed, stop, b1, true, b3, i)
IDLE₇(fl, d, m, b1, b2, b3, empty) -> BUSY₇(fl, d, m, b1, b2, b3, empty)
BUSY₇(BF, closed, up, b1, b2, b3, i) -> IDLE₇(F, closed, up, b1, b2, b3, i)
BUSY₇(S, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, stop, b1, b2, b3, i)
BUSY₇(B, closed, up, false, b2, b3, i) -> IDLE₇(BF, closed, up, false, b2, b3, i)
BUSY₇(S, closed, down, b1, b2, false, i) -> IDLE₇(FS, closed, down, b1, b2, false, i)
BUSY₇(B, closed, up, true, b2, b3, i) -> IDLE₇(B, closed, stop, true, b2, b3, i)
BUSY₇(FS, closed, up, b1, b2, b3, i) -> IDLE₇(S, closed, up, b1, b2, b3, i)
BUSY₇(B, closed, down, b1, b2, b3, i) -> IDLE₇(B, closed, stop, b1, b2, b3, i)

The TRS R consists of the following rules:

start₁(i) -> busy₇(F, closed, stop, false, false, false, i)
busy₇(BF, d, stop, b1, b2, b3, i) -> incorrect
busy₇(FS, d, stop, b1, b2, b3, i) -> incorrect
busy₇(fl, open, up, b1, b2, b3, i) -> incorrect
busy₇(fl, open, down, b1, b2, b3, i) -> incorrect
busy₇(B, closed, stop, false, false, false, empty) -> correct
busy₇(F, closed, stop, false, false, false, empty) -> correct
busy₇(S, closed, stop, false, false, false, empty) -> correct
busy₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(B, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(F, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i)) -> idle₇(S, closed, stop, false, false, false, newbuttons₄(i1, i2, i3, i))
busy₇(B, open, stop, false, b2, b3, i) -> idle₇(B, closed, stop, false, b2, b3, i)
busy₇(F, open, stop, b1, false, b3, i) -> idle₇(F, closed, stop, b1, false, b3, i)
busy₇(S, open, stop, b1, b2, false, i) -> idle₇(S, closed, stop, b1, b2, false, i)
busy₇(B, d, stop, true, b2, b3, i) -> idle₇(B, open, stop, false, b2, b3, i)
busy₇(F, d, stop, b1, true, b3, i) -> idle₇(F, open, stop, b1, false, b3, i)
busy₇(S, d, stop, b1, b2, true, i) -> idle₇(S, open, stop, b1, b2, false, i)
busy₇(B, closed, down, b1, b2, b3, i) -> idle₇(B, closed, stop, b1, b2, b3, i)
busy₇(S, closed, up, b1, b2, b3, i) -> idle₇(S, closed, stop, b1, b2, b3, i)
busy₇(B, closed, up, true, b2, b3, i) -> idle₇(B, closed, stop, true, b2, b3, i)
busy₇(F, closed, up, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(F, closed, down, b1, true, b3, i) -> idle₇(F, closed, stop, b1, true, b3, i)
busy₇(S, closed, down, b1, b2, true, i) -> idle₇(S, closed, stop, b1, b2, true, i)
busy₇(B, closed, up, false, b2, b3, i) -> idle₇(BF, closed, up, false, b2, b3, i)
busy₇(F, closed, up, b1, false, b3, i) -> idle₇(FS, closed, up, b1, false, b3, i)
busy₇(F, closed, down, b1, false, b3, i) -> idle₇(BF, closed, down, b1, false, b3, i)
busy₇(S, closed, down, b1, b2, false, i) -> idle₇(FS, closed, down, b1, b2, false, i)
busy₇(BF, closed, up, b1, b2, b3, i) -> idle₇(F, closed, up, b1, b2, b3, i)
busy₇(BF, closed, down, b1, b2, b3, i) -> idle₇(B, closed, down, b1, b2, b3, i)
busy₇(FS, closed, up, b1, b2, b3, i) -> idle₇(S, closed, up, b1, b2, b3, i)
busy₇(FS, closed, down, b1, b2, b3, i) -> idle₇(F, closed, down, b1, b2, b3, i)
busy₇(B, closed, stop, false, true, b3, i) -> idle₇(B, closed, up, false, true, b3, i)
busy₇(B, closed, stop, false, false, true, i) -> idle₇(B, closed, up, false, false, true, i)
busy₇(F, closed, stop, true, false, b3, i) -> idle₇(F, closed, down, true, false, b3, i)
busy₇(F, closed, stop, false, false, true, i) -> idle₇(F, closed, up, false, false, true, i)
busy₇(S, closed, stop, b1, true, false, i) -> idle₇(S, closed, down, b1, true, false, i)
busy₇(S, closed, stop, true, false, false, i) -> idle₇(S, closed, down, true, false, false, i)
idle₇(fl, d, m, b1, b2, b3, empty) -> busy₇(fl, d, m, b1, b2, b3, empty)
idle₇(fl, d, m, b1, b2, b3, newbuttons₄(i1, i2, i3, i)) -> busy₇(fl, d, m, or₂(b1, i1), or₂(b2, i2), or₂(b3, i3), i)
or₂(true, b) -> true
or₂(false, b) -> b

The set Q consists of the following terms:

start₁(x0)
busy₇(BF, x0, stop, x1, x2, x3, x4)
busy₇(FS, x0, stop, x1, x2, x3, x4)
busy₇(x0, open, up, x1, x2, x3, x4)
busy₇(x0, open, down, x1, x2, x3, x4)
busy₇(B, closed, stop, false, false, false, empty)
busy₇(F, closed, stop, false, false, false, empty)
busy₇(S, closed, stop, false, false, false, empty)
busy₇(B, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(F, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(S, closed, stop, false, false, false, newbuttons₄(x0, x1, x2, x3))
busy₇(B, open, stop, false, x0, x1, x2)
busy₇(F, open, stop, x0, false, x1, x2)
busy₇(S, open, stop, x0, x1, false, x2)
busy₇(B, x0, stop, true, x1, x2, x3)
busy₇(F, x0, stop, x1, true, x2, x3)
busy₇(S, x0, stop, x1, x2, true, x3)
busy₇(B, closed, down, x0, x1, x2, x3)
busy₇(S, closed, up, x0, x1, x2, x3)
busy₇(B, closed, up, true, x0, x1, x2)
busy₇(F, closed, up, x0, true, x1, x2)
busy₇(F, closed, down, x0, true, x1, x2)
busy₇(S, closed, down, x0, x1, true, x2)
busy₇(B, closed, up, false, x0, x1, x2)
busy₇(F, closed, up, x0, false, x1, x2)
busy₇(F, closed, down, x0, false, x1, x2)
busy₇(S, closed, down, x0, x1, false, x2)
busy₇(BF, closed, up, x0, x1, x2, x3)
busy₇(BF, closed, down, x0, x1, x2, x3)
busy₇(FS, closed, up, x0, x1, x2, x3)
busy₇(FS, closed, down, x0, x1, x2, x3)
busy₇(B, closed, stop, false, true, x0, x1)
busy₇(B, closed, stop, false, false, true, x0)
busy₇(F, closed, stop, true, false, x0, x1)
busy₇(F, closed, stop, false, false, true, x0)
busy₇(S, closed, stop, x0, true, false, x1)
busy₇(S, closed, stop, true, false, false, x0)
idle₇(x0, x1, x2, x3, x4, x5, empty)
idle₇(x0, x1, x2, x3, x4, x5, newbuttons₄(x6, x7, x8, x9))
or₂(true, x0)
or₂(false, x0)

We have to consider all minimal (P,Q,R)-chains.